COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00012 ENDMK
C⊗;

.device  xgp
.FONT 1 "baxl30";		<<normal font>>
.FONT 3 "BAXI30[j,red]"	<<mexpr font:basi30+>>
.FONT a "bdr40";		<<chapter titles and numbers>>
.begin double space; turn on "%#"
.group  skip 6
.once center
%aGenerating Correct Programs from Logic Specifications%1
.group skip 1
.once center
by Ruth E. Davis
.group skip 6;
#####The "programming problem" is one of obtaining correct programs.
The desire to prove the correctness of programs led to the development of program
verification techniques; however, attempts at verification have been less successful
 than some had hoped.
 
#####In analyzing the situation, we came to feel
that the flaw is in the approach. In program verification one typically proves
correctness by deriving logic "specifications" from the program and proving that
the program meets these specifications.  We believe one should write
the specifications first, and derive the program from them in such a way as
to guarantee that the derived program satisfies the specifications. 
The specification should be written in a high level language that enables one
to describe what is to be accomplished, indicating functional relationships
without having to consider computational details.  Such a specification, in
which only the abstract description of the problem is required, is less prone
to error than a typical programming language specification in which every detail of the 
computation must be provided.

#####It is our thesis that the generation of an algorithm is a target-language-independent
process.  We have implemented a system to generate programs from logic specifications.
The specifications are first translated into an intermediate language
and then a program is generated from the intermediate form.
The specification
language for this system includes a subset of first-order Predicate
Calculus known as Horn Clauses.
The specifications we require are "descriptive" in that
they specify the logic of the program without specifying the control, but they are
also, in part, "computational" in that the Horn clauses could be "run" as programs
given a complete theorem prover, or logic interpreter.

#####The system was implemented in MACLISP on a DEC KL10 at the Stanford Artificial
Intelligence Laboratory.  In the dissertation we describe the implementation
and prove that it provides a valid way to derive correct programs. This is
accomplished by proving that the top level mappings from specification to
intermediate language to target program (the proof is for the mapping to LISP)
are correct; we do not prove the entire implementation is correct.

#####We begin by giving a brief history of the approaches taken by other investigators
in this area, and then describe the system invented by the author.
We formally describe the specification language via a
context-free description of the syntax
and an axiomatic specification of the semantics.
The relationship between a specification and a program written for a logic
interpreter is discussed.

#####We then describe the intermediate language in detail, again supplying a context-free
grammar for the syntax, and the axiomatic semantics.
The mapping from specification language to intermediate language is described
and we prove that this mapping
preserves the axiomatic semantics of the specifications.
The mapping from the intermediate language
to LISP is then described and proven correct.

#####The system can be extended to handle generation of
programs in several languages.
The implementations for LISP and Pascal are discussed, and a set of guidelines
are given for adding more languages to the system.

#####The appendices include several sample specifications and the programs generated
from them, the specification of a program generation system, and the listing
of the entire system along with the code that implements the generation of programs
in LISP and Pascal.

#####The system described is unique in its ability to generate programs in more than
one language. The rules provided explain how to construct the additions
required for any new language.
We can generate the system itself from its specification,
exhibiting its ability to handle large programs, and
making it immediately portable.
 More importantly, the system provides a means of
obtaining correct programs that is decidedly less painful than verification.
The user is still required to specify the logic of a program, but the language
used in the specification frees the user from concerns of representation and
implementation.

 



.end